'''
Created on Sep 8, 2011

@author: nktran
'''
import re
import os
import sys

from constant import QUERY_FILE, ALPHABET_FILE, INSTANCE_FILE, TABLE_FILE
from fsa import FSA

class Angluin_V2:
    """
    Version 2.0 Implementation of Angluin algorithm
    Automatically answer membership queries and counter-examples
    1. For membership queries:
        @return: True if the query is in the instance file
    2. For counter-example:
        @return: example in the instance file that is not accepted by acceptor
        @improve: using negative examples to adjust acceptor
    """
    
    def __init__(self, ext):
        """
        Default constructor with an extension
        
        @param ext: files extension
        @var table: store the value of {0,1} that means the string {prefix+suffix} is
        in unknown language or not.
        @var prefix: are rows of the table also are prefix of strings
        @var suffix: are columns of the table also are suffix of strings
        @var alphabet: alphabets of the unknown grammar
        @var query: contains all queries already asked
        @var instance: contains all       
        """
        self.__lamda = ""
        self.__mquery = 0
        self.__cquery = 0
        self.__ext__ = ext
        
        self.table = dict()
        self.prefix = set()
        self.suffix = set()
        self.alphabet = set()
        self.query = dict()
        self.instance = set()        

    def __init_table(self):
        """
        @requires: instance.[ext], alphabet.[ext] files
        @return: table with initial values
        """
        self.prefix.add(self.__lamda)
        self.suffix.add(self.__lamda)
        self.set_alphabet()
        self.set_instance()
        
        ans = self.__get_answer('_lamda_')
        self.__mquery = self.__mquery + 1        
        if ans == 'y':
            self.table[self.__lamda] = {self.__lamda:1}
            self.query[self.__lamda] = 1
        else:
            self.table[self.__lamda] = {self.__lamda:0}
            self.query[self.__lamda] = 0
        
        for a in self.alphabet:
            ans = self.__get_answer(a)
            self.__mquery = self.__mquery + 1
            if ans == 'y':
                self.table[a] = {self.__lamda:1}
                self.query[a] = 1
            else:                
                self.table[a] = {self.__lamda:0}
                self.query[a] = 0        
       
    def set_alphabet(self):
        """
        @return: alphabet from the file
        """
        fname = ALPHABET_FILE + self.__ext__
        self.alphabet = self.read_file(fname,'\s+')   

    def set_instance(self):
        """
        @return: instances from the file
        """
        fname = INSTANCE_FILE + self.__ext__
        self.instance = self.read_file(fname,'\n')
        
    def read_file(self, fname, delim):
        """
        @return: context in the file name (fname) with the delimiter delim
        """
        if fname not in os.listdir("."):
            print fname, 'does not exist!!!'
            sys.exit(1)
            
        result = set()
        fin = open(fname, 'r')
        try:
            lines = re.split(delim, fin.read())
            for line in lines:
                if len(line.strip()) == 0: continue
                result.add(line)
        finally:
            fin.close()
        
        return result                
    
    def __find_new_suffix(self):
        """
        Find prefix pre1 and pre2, alphabet a and suffix suf such that
        row(pre1) = row(pre2) and T(pre1+a+suf) != T(pre2+a+suf)
        
        @return: a+suf
        """
        for pre1 in self.prefix:
            for pre2 in self.prefix:                        
                if pre1 != pre2 and self.table[pre1] == self.table[pre2]:
                    for suf in self.suffix:                                
                        for a in self.alphabet:
                            if self.table[pre1+a][suf] != self.table[pre2+a][suf] \
                                    and a+suf not in self.suffix:
                                return a+suf
        return None
    
    def __find_new_prefix(self):
        """
        Find prefix pre1 and alphabet a such that row(pre1+a) is different 
        from row(pre) for all pre in prefix set
        
        @return: pref + a
        """
        for pre1 in self.prefix:
            for a in self.alphabet:
                if pre1+a in self.prefix:
                    continue
                flag = True
                has_key = self.table.has_key(pre1+a)                            
                for pre in self.prefix:
                    if has_key and self.table[pre1+a] == self.table[pre]:
                        flag = False
                        break
                if flag:
                    return pre1+a   
        return None
    
    def learn(self):
        """
        Learn finite state automata that accept an unknown regular language
        using an oracle: membership queries and counter example
        @param: 
        @return: acceptor
        """
        self.__init_table()
        
        number = 0
        print 'Start learning...'
        while True:
            new_suffix_item = self.__find_new_suffix()
            new_prefix_item = self.__find_new_prefix()       
            while new_suffix_item != None or new_prefix_item != None:
                if new_suffix_item != None:
                    self.__print_file('Table %d is not consistent!' % (number))
                    print 'Table %d is not consistent' % (number)
                    # find a in alphabet and suf in suffix set
                    self.suffix.add(new_suffix_item)
                    # Debugging
                    string = 'Adding %s into suffix set' % (new_suffix_item)
                    print 'Adding %s into suffix set\n' % (new_suffix_item)
                    self.__print_file(string)
                    self.__print_set('prefix', self.prefix)
                    self.__print_set('suffix', self.suffix)                    
                    # update table after adding new elements into suffix set
                    self.__update_suffix(set([new_suffix_item]))
                    # Debugging                   
                    number = number + 1
                    self.__print_table(number)                    

                if new_prefix_item != None:
                    self.__print_file('Table %d is not closed!' % (number))
                    print 'Table %d is not closed!' % (number)
                    # find pre in prefix set and a in alphabet
                    self.prefix.add(new_prefix_item)
                    # Debugging
                    string = 'Adding %s into prefix set' % (new_prefix_item)
                    print 'Adding %s into prefix set\n' % (new_prefix_item)
                    self.__print_file(string)
                    self.__print_set('prefix', self.prefix)
                    self.__print_set('suffix', self.suffix)
                    # Update table after adding new elements into prefix set
                    self.__update_prefix(set([new_prefix_item]))
                    # Debugging
                    number = number + 1
                    self.__print_table(number)                                                            
                # end if
                new_suffix_item = self.__find_new_suffix()
                new_prefix_item = self.__find_new_prefix()            
            # end membership queries
            
            print 'Table %d is closed and consistent.' % (number)
            self.__print_file('#Table %d is closed and consistent.' % (number))
            
            acceptor = FSA()
            acceptor.construct(self)
#            acceptor.toString()
            
            counter_example = self.__find_counter_example(acceptor, self.instance)
#            if number >= 3:
#                break
            print 'Find new counter example: %s\n' % (counter_example)
            if counter_example == None:
                return acceptor
            self.__add_cx_to_table(counter_example)
            
            number = number + 1
            self.__print_table(number)                    
                
    def __find_counter_example(self, acceptor, instances):
        """
        @return: counter-example
        """
        for inst in sorted(instances):
            if not acceptor.parse(inst):
                return inst
        return None
    
    def __add_cx_to_table(self, counter_example=None):
        """
        Adding the counter example to the table
        @note: Adding all prefix and itself
        """
        if counter_example == None:
            return
        new_prefix_set = set()
        pre = ""
        for substr in re.split('\s+', counter_example):
            pre = pre + substr
            new_prefix_set.add(pre)
            self.prefix.add(pre)
            
        self.__update_prefix(new_prefix_set)
    
    def __update_suffix(self, new_suffix_set):
        """
        Update the table with a new suffix set
        @return: new table
        """
        for pre in self.prefix:
            # prefix
            for suf in new_suffix_set:
                if not self.query.has_key(pre+suf):
                    self.__new_query(pre,suf)
                else:
                    self.__add_to_table(pre, suf, self.query[pre+suf])
            # prefix + alphabet
            for a in self.alphabet:
                for suf in new_suffix_set:
                    if not self.query.has_key(pre+a+suf):
                        self.__new_query(pre+a, suf)
                    else:
                        self.__add_to_table(pre+a, suf, self.query[pre+a+suf])                   
        
    
    def __update_prefix(self, new_prefix_set):
        """
        Update the table with a new preffix set
        @return: new table        
        """
        for pre in new_prefix_set:
            # prefix
            for suf in self.suffix:
                if not self.query.has_key(pre+suf):
                    self.__new_query(pre, suf)
                else:
                    self.__add_to_table(pre, suf, self.query[pre+suf])
            # prefix + suffix
            for a in self.alphabet:
                for suf in self.suffix:
                    if not self.query.has_key(pre+a+suf):
                        self.__new_query(pre+a, suf)
                    else:
                        self.__add_to_table(pre+a, suf, self.query[pre+a+suf])
    def __add_to_table(self, pre, suf, val):
        """
        Adding the cell [pre, suf] with the value val
        """
        if self.table.has_key(pre):
            self.table[pre][suf] = val
        else:
            self.table[pre] = {suf:val}

    def __get_answer(self, query):
        """
        @return: True if the query is in the instance file
        """
        for inst in self.instance:
            temp = ""
            for substr in re.split("\s+", inst):
                temp = temp + substr
            if temp == query:
                self.__print_query(query, 'yes')
                return 'y'
                    
        self.__print_query(query, 'no')
        return 'n'
    
    def __new_query(self, pre, suf):
        """
        @note: asking new membership query
        """
        ans = self.__get_answer(pre + suf)
        self.__mquery = self.__mquery + 1
        if ans == 'y':
            self.__add_to_table(pre, suf, 1)
            self.query[pre+suf] = 1
        else:
            self.__add_to_table(pre, suf, 0)
            self.query[pre+suf] = 0
        
    def __print_file(self, query):
        """
        @note: for debugging, print to query file a query
        """
        fout = open(QUERY_FILE + self.__ext__, 'a')
        try:
            fout.write(query + '\n')
        finally:
            fout.close()
            
    def __print_set(self, string, inSet):
        """
        @note: for debugging, print a set into query file
        """
        fout = open(QUERY_FILE + self.__ext__, 'a')
        fout.write(string + ':')
        try:
            for e in inSet:
                fout.write(self.__format(e) + ' ')                
            fout.write('\n')
        finally:
            fout.close()        
    
    def __print_table(self, number):
        """
        @note: for debugging, print the table into table file
        """
        fout = open(TABLE_FILE + self.__ext__, 'a')
        try:
            fout.write("# Table " + str(number) + '\n' )
            fout.write("Prefix: {")
            for pre in self.prefix:
                fout.write(self.__format(pre) + ', ')
            fout.write("}")
            fout.write("\n Suffix: {")
            for suf in self.suffix:
                fout.write(self.__format(suf) + ', ')
            fout.write("}\n")                            
            for key in self.table.keys():
                for val in self.table[key].keys():
                    fout.write('T[' + self.__format(key) + '+' + self.__format(val) + ']=T[' + 
                               key + val + ']' +  '=' + str(self.table[key][val]) + '\t  ')
                fout.write('\n')
            fout.write('\n')
        finally:
            fout.close()
        
    def __print_query(self, query, ans):
        """
        @note: for debugging, print query with the answer into query file
        """
        fout = open (QUERY_FILE + self.__ext__, 'a')
        try:
            fout.write('query= ' + query)
            fout.write('\t\tin_language = ' + ans)
            fout.write('\n')
        finally:
            fout.close()
            
    def __format(self,string):
        """
        @return: new format of the string
        """
        if string == "":
            return "_lamda_"        
        return string    
        